Inference at * 2 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. (i:{0..(||L1|| - 1)}. (x = L1[i] & y = L1[(i+1)]))
6.  ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
6.  (i:{0..(||L2|| - 1)}. (x = L2[i] & y = L2[(i+1)]))
  i:{0..(||L1 @ L2|| - 1)}. (x = (L1 @ L2)[i] & y = (L1 @ L2)[(i+1)]) 

latex

 by ((SplitOrHyps) 
CollapseTHEN (ExRepD)) 

latex

C1: 

C1: 6. i : {0..(||L1|| - 1)}
C1: 7. x = L1[i]
C1: 8. y = L1[(i+1)]
C1:   i:{0..(||L1 @ L2|| - 1)}. (x = (L1 @ L2)[i] & y = (L1 @ L2)[(i+1)])
C2: 

C2: 6. 0 < ||L1||
C2: 7. 0 < ||L2||
C2: 8. x = last(L1)
C2: 9. y = hd(L2)
C2:   i:{0..(||L1 @ L2|| - 1)}. (x = (L1 @ L2)[i] & y = (L1 @ L2)[(i+1)])
C3: 

C3: 6. i : {0..(||L2|| - 1)}
C3: 7. x = L2[i]
C3: 8. y = L2[(i+1)]
C3:   i:{0..(||L1 @ L2|| - 1)}. (x = (L1 @ L2)[i] & y = (L1 @ L2)[(i+1)])
C.

Definitions

P  Q, left + right, x:A. B(x), P & Q, x:A  B(x)